\begin{tabbing}
es{-}sends{-}iff2(${\it es}$;$l$;${\it tg}$;$B$;${\it ds}$;$e$.$P$($e$);$e$.$f$($e$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$:E. kind($e$) $=$ rcv($l$,${\it tg}$) $\Rightarrow$ valtype($e$) $\subseteq\rho$ $B$)\+
\\[0ex]\& ($\forall$$x$:Id. vartype(source($l$);$x$) $\subseteq\rho$ ${\it ds}$($x$)?Top)
\\[0ex]\& \=$\forall$$e$@source($l$). $P$($e$) $\Rightarrow$ ($\exists$${\it e'}$:E. kind(${\it e'}$) $=$ rcv($l$,${\it tg}$) \& sender(${\it e'}$) $=$ $e$)\+
\\[0ex]\& ($\forall$${\it e'}$:E. kind(${\it e'}$) $=$ rcv($l$,${\it tg}$) $\Rightarrow$ $P$(sender(${\it e'}$)) \& val(${\it e'}$) $=$ $f$(sender(${\it e'}$)))
\\[0ex]\& (\=$\forall$${\it e'}$:E.\+
\\[0ex]kind(${\it e'}$) $=$ rcv($l$,${\it tg}$)
\\[0ex]$\Rightarrow$ ($\forall$${\it e''}$:E. isrcv(${\it e''}$) $\Rightarrow$ lnk(${\it e''}$) $=$ $l$ $\Rightarrow$ sender(${\it e''}$) $=$ sender(${\it e'}$) $\Rightarrow$ ${\it e''}$ $=$ ${\it e'}$))
\-\-\-
\end{tabbing}